\begin{tabbing}
$\forall$\=$A$, $C$, $B$:Type, ${\it eqa}$:EqDecider($A$), ${\it eqc}$, ${\it eqc'}$:EqDecider($C$), $r$:($A$$\rightarrow$$C$), $f$:$a$:$A$ fp$\rightarrow$ $B$, $a$:$A$, $z$:$B$,\+
\\[0ex]$c$:$C$.
\-\\[0ex]Inj($A$; $C$; $r$) $\Rightarrow$ $c$ $=$ $r$($a$) $\Rightarrow$ rename($r$;$f$)($c$)?$z$ $=$ $f$($a$)?$z$ $\in$ $B$
\end{tabbing}